Termination proof of /tmp/tmpTWWZiP/List1.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 493 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIDPv1Proof (⇒, 79 ms)

        ↳7 IDP

        ↳8 IDPtoQDPProof (⇒, 48 ms)

        ↳9 QDP

        ↳10 QDPSizeChangeProof (⇔, 0 ms)

        ↳11 YES

    ↳12 JBCTerminationSCC

        ↳13 SCCToIDPv1Proof (⇒, 102 ms)

        ↳14 IDP

        ↳15 IDPNonInfProof (⇒, 136 ms)

        ↳16 AND

            ↳17 IDP

                ↳18 IDependencyGraphProof (⇔, 0 ms)

                ↳19 TRUE

            ↳20 IDP

                ↳21 IDependencyGraphProof (⇔, 0 ms)

                ↳22 TRUE

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_26 (Sun Microsystems Inc.) Main-Class: List1

public class List1 {
	List1 pred, next;

	List1(List1 pred) {
		if (pred != null) {
			pred.next = this;
		}
		this.pred = pred;
	}

	static int length(List1 l) {
		int r = 1;
		while (null != (l = l.next))
			r++;
		return r;
	}

	public static void main(String[] args) {
		//Create doubly-linked list:
		int length = args.length;
		List1 cur = new List1(null);
		List1 first = cur;
		while (length-- > 0) {
			cur = new List1(cur);
		}

		length(first);		
	}
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
List1.main([Ljava/lang/String;)V: Graph of 108 nodes with 2 SCCs.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 2 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: List1.main([Ljava/lang/String;)V
SCC calls the following helper methods:
Performed SCC analyses: UsedFieldsAnalysis

(6) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 18 rules for P and 0 rules for R.

P rules:
2457_0_length_Load(EOS(STATIC_2457), java.lang.Object(o448sub), java.lang.Object(o447sub)) → 2458_0_length_FieldAccess(EOS(STATIC_2458), java.lang.Object(o448sub), java.lang.Object(o447sub))
2458_0_length_FieldAccess(EOS(STATIC_2458), java.lang.Object(o448sub), java.lang.Object(o447sub)) → 2460_0_length_FieldAccess(EOS(STATIC_2460), java.lang.Object(o448sub), java.lang.Object(o447sub))
2458_0_length_FieldAccess(EOS(STATIC_2458), java.lang.Object(o448sub), java.lang.Object(o448sub)) → 2461_0_length_FieldAccess(EOS(STATIC_2461), java.lang.Object(o448sub), java.lang.Object(o448sub))
2460_0_length_FieldAccess(EOS(STATIC_2460), java.lang.Object(o448sub), java.lang.Object(List1(EOC, o456))) → 2462_0_length_FieldAccess(EOS(STATIC_2462), java.lang.Object(o448sub), java.lang.Object(List1(EOC, o456)))
2462_0_length_FieldAccess(EOS(STATIC_2462), java.lang.Object(o448sub), java.lang.Object(List1(EOC, o456))) → 2465_0_length_Duplicate(EOS(STATIC_2465), java.lang.Object(o448sub), o456)
2465_0_length_Duplicate(EOS(STATIC_2465), java.lang.Object(o448sub), o456) → 2468_0_length_Store(EOS(STATIC_2468), java.lang.Object(o448sub), o456, o456)
2468_0_length_Store(EOS(STATIC_2468), java.lang.Object(o448sub), o456, o456) → 2471_0_length_EQ(EOS(STATIC_2471), java.lang.Object(o448sub), o456, o456)
2471_0_length_EQ(EOS(STATIC_2471), java.lang.Object(o448sub), java.lang.Object(o469sub), java.lang.Object(o469sub)) → 2475_0_length_EQ(EOS(STATIC_2475), java.lang.Object(o448sub), java.lang.Object(o469sub), java.lang.Object(o469sub))
2475_0_length_EQ(EOS(STATIC_2475), java.lang.Object(o448sub), java.lang.Object(o469sub), java.lang.Object(o469sub)) → 2477_0_length_Inc(EOS(STATIC_2477), java.lang.Object(o448sub), java.lang.Object(o469sub))
2477_0_length_Inc(EOS(STATIC_2477), java.lang.Object(o448sub), java.lang.Object(o469sub)) → 2479_0_length_JMP(EOS(STATIC_2479), java.lang.Object(o448sub), java.lang.Object(o469sub))
2479_0_length_JMP(EOS(STATIC_2479), java.lang.Object(o448sub), java.lang.Object(o469sub)) → 2483_0_length_ConstantStackPush(EOS(STATIC_2483), java.lang.Object(o448sub), java.lang.Object(o469sub))
2483_0_length_ConstantStackPush(EOS(STATIC_2483), java.lang.Object(o448sub), java.lang.Object(o469sub)) → 2455_0_length_ConstantStackPush(EOS(STATIC_2455), java.lang.Object(o448sub), java.lang.Object(o469sub))
2455_0_length_ConstantStackPush(EOS(STATIC_2455), java.lang.Object(o448sub), java.lang.Object(o447sub)) → 2457_0_length_Load(EOS(STATIC_2457), java.lang.Object(o448sub), java.lang.Object(o447sub))
2461_0_length_FieldAccess(EOS(STATIC_2461), java.lang.Object(List1(EOC, o459)), java.lang.Object(List1(EOC, o459))) → 2463_0_length_FieldAccess(EOS(STATIC_2463), java.lang.Object(List1(EOC, o459)), java.lang.Object(List1(EOC, o459)))
2463_0_length_FieldAccess(EOS(STATIC_2463), java.lang.Object(List1(EOC, o459)), java.lang.Object(List1(EOC, o459))) → 2466_0_length_Duplicate(EOS(STATIC_2466), java.lang.Object(List1(EOC, o459)), o459)
2466_0_length_Duplicate(EOS(STATIC_2466), java.lang.Object(List1(EOC, o459)), o459) → 2469_0_length_Store(EOS(STATIC_2469), java.lang.Object(List1(EOC, o459)), o459, o459)
2469_0_length_Store(EOS(STATIC_2469), java.lang.Object(List1(EOC, o459)), o459, o459) → 2473_0_length_EQ(EOS(STATIC_2473), java.lang.Object(List1(EOC, o459)), o459, o459)
2473_0_length_EQ(EOS(STATIC_2473), java.lang.Object(List1(EOC, o459)), o459, o459) → 2471_0_length_EQ(EOS(STATIC_2471), java.lang.Object(List1(EOC, o459)), o459, o459)
R rules:

Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.

P rules:
2457_0_length_Load(EOS(STATIC_2457), java.lang.Object(x0), java.lang.Object(List1(EOC, java.lang.Object(x1)))) → 2457_0_length_Load(EOS(STATIC_2457), java.lang.Object(x0), java.lang.Object(x1))
2457_0_length_Load(EOS(STATIC_2457), java.lang.Object(List1(EOC, java.lang.Object(x0))), java.lang.Object(List1(EOC, java.lang.Object(x0)))) → 2457_0_length_Load(EOS(STATIC_2457), java.lang.Object(List1(EOC, java.lang.Object(x0))), java.lang.Object(x0))
R rules:

Filtered ground terms:

2457_0_length_Load(x1, x2, x3) → 2457_0_length_Load(x2, x3)
List1(x1, x2) → List1(x2)
EOS(x1) → EOS

Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.

P rules:
2457_0_length_Load(java.lang.Object(x0), java.lang.Object(List1(java.lang.Object(x1)))) → 2457_0_length_Load(java.lang.Object(x0), java.lang.Object(x1))
2457_0_length_Load(java.lang.Object(List1(java.lang.Object(x0))), java.lang.Object(List1(java.lang.Object(x0)))) → 2457_0_length_Load(java.lang.Object(List1(java.lang.Object(x0))), java.lang.Object(x0))
R rules:

Finished conversion. Obtained 2 rules for P and 0 rules for R. System has no predefined symbols.

P rules:
2457_0_LENGTH_LOAD(java.lang.Object(x0), java.lang.Object(List1(java.lang.Object(x1)))) → 2457_0_LENGTH_LOAD(java.lang.Object(x0), java.lang.Object(x1))
2457_0_LENGTH_LOAD(java.lang.Object(List1(java.lang.Object(x0))), java.lang.Object(List1(java.lang.Object(x0)))) → 2457_0_LENGTH_LOAD(java.lang.Object(List1(java.lang.Object(x0))), java.lang.Object(x0))
R rules:

(7) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:
none

R is empty.

The integer pair graph contains the following rules and edges:
(0): 2457_0_LENGTH_LOAD(java.lang.Object(x0[0]), java.lang.Object(List1(java.lang.Object(x1[0])))) → 2457_0_LENGTH_LOAD(java.lang.Object(x0[0]), java.lang.Object(x1[0]))
(1): 2457_0_LENGTH_LOAD(java.lang.Object(List1(java.lang.Object(x0[1]))), java.lang.Object(List1(java.lang.Object(x0[1])))) → 2457_0_LENGTH_LOAD(java.lang.Object(List1(java.lang.Object(x0[1]))), java.lang.Object(x0[1]))

(0) -> (0), if (java.lang.Object(x0[0]) →^* java.lang.Object(x0[0]')∧java.lang.Object(x1[0]) →^* java.lang.Object(List1(java.lang.Object(x1[0]'))))

(0) -> (1), if (java.lang.Object(x0[0]) →^* java.lang.Object(List1(java.lang.Object(x0[1])))∧java.lang.Object(x1[0]) →^* java.lang.Object(List1(java.lang.Object(x0[1]))))

(1) -> (0), if (java.lang.Object(List1(java.lang.Object(x0[1]))) →^* java.lang.Object(x0[0])∧java.lang.Object(x0[1]) →^* java.lang.Object(List1(java.lang.Object(x1[0]))))

(1) -> (1), if (java.lang.Object(List1(java.lang.Object(x0[1]))) →^* java.lang.Object(List1(java.lang.Object(x0[1]')))∧java.lang.Object(x0[1]) →^* java.lang.Object(List1(java.lang.Object(x0[1]'))))

The set Q is empty.

(8) IDPtoQDPProof (SOUND transformation)

Represented integers and predefined function symbols by Terms

(9) Obligation:

Q DP problem:
The TRS P consists of the following rules:

2457_0_LENGTH_LOAD(java.lang.Object(x0[0]), java.lang.Object(List1(java.lang.Object(x1[0])))) → 2457_0_LENGTH_LOAD(java.lang.Object(x0[0]), java.lang.Object(x1[0]))
2457_0_LENGTH_LOAD(java.lang.Object(List1(java.lang.Object(x0[1]))), java.lang.Object(List1(java.lang.Object(x0[1])))) → 2457_0_LENGTH_LOAD(java.lang.Object(List1(java.lang.Object(x0[1]))), java.lang.Object(x0[1]))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(10) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

2457_0_LENGTH_LOAD(java.lang.Object(x0[0]), java.lang.Object(List1(java.lang.Object(x1[0])))) → 2457_0_LENGTH_LOAD(java.lang.Object(x0[0]), java.lang.Object(x1[0]))
The graph contains the following edges 1 >= 1, 2 > 2
2457_0_LENGTH_LOAD(java.lang.Object(List1(java.lang.Object(x0[1]))), java.lang.Object(List1(java.lang.Object(x0[1])))) → 2457_0_LENGTH_LOAD(java.lang.Object(List1(java.lang.Object(x0[1]))), java.lang.Object(x0[1]))
The graph contains the following edges 1 >= 1, 2 >= 1, 1 > 2, 2 > 2

(11) YES

(12) Obligation:

(13) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 32 rules for P and 0 rules for R.

P rules:
677_0_main_Inc(EOS(STATIC_677), i88, i88) → 679_0_main_LE(EOS(STATIC_679), +(i88, -1), i88)
679_0_main_LE(EOS(STATIC_679), i93, i97) → 683_0_main_LE(EOS(STATIC_683), i93, i97)
683_0_main_LE(EOS(STATIC_683), i93, i97) → 687_0_main_New(EOS(STATIC_687), i93) | >(i97, 0)
687_0_main_New(EOS(STATIC_687), i93) → 690_0_main_Duplicate(EOS(STATIC_690), i93)
690_0_main_Duplicate(EOS(STATIC_690), i93) → 694_0_main_Load(EOS(STATIC_694), i93)
694_0_main_Load(EOS(STATIC_694), i93) → 696_0_main_InvokeMethod(EOS(STATIC_696), i93)
696_0_main_InvokeMethod(EOS(STATIC_696), i93) → 700_0_<init>_Load(EOS(STATIC_700), i93)
700_0_<init>_Load(EOS(STATIC_700), i93) → 707_0_<init>_InvokeMethod(EOS(STATIC_707), i93)
707_0_<init>_InvokeMethod(EOS(STATIC_707), i93) → 714_0_<init>_Load(EOS(STATIC_714), i93)
714_0_<init>_Load(EOS(STATIC_714), i93) → 719_0_<init>_NULL(EOS(STATIC_719), i93)
719_0_<init>_NULL(EOS(STATIC_719), i93) → 724_0_<init>_Load(EOS(STATIC_724), i93)
724_0_<init>_Load(EOS(STATIC_724), i93) → 729_0_<init>_Load(EOS(STATIC_729), i93)
729_0_<init>_Load(EOS(STATIC_729), i93) → 739_0_<init>_FieldAccess(EOS(STATIC_739), i93)
739_0_<init>_FieldAccess(EOS(STATIC_739), i93) → 744_0_<init>_FieldAccess(EOS(STATIC_744), i93)
739_0_<init>_FieldAccess(EOS(STATIC_739), i93) → 745_0_<init>_FieldAccess(EOS(STATIC_745), i93)
744_0_<init>_FieldAccess(EOS(STATIC_744), i93) → 749_0_<init>_Load(EOS(STATIC_749), i93)
749_0_<init>_Load(EOS(STATIC_749), i93) → 761_0_<init>_Load(EOS(STATIC_761), i93)
761_0_<init>_Load(EOS(STATIC_761), i93) → 772_0_<init>_FieldAccess(EOS(STATIC_772), i93)
772_0_<init>_FieldAccess(EOS(STATIC_772), i93) → 786_0_<init>_Return(EOS(STATIC_786), i93)
786_0_<init>_Return(EOS(STATIC_786), i93) → 805_0_main_Store(EOS(STATIC_805), i93)
805_0_main_Store(EOS(STATIC_805), i93) → 814_0_main_JMP(EOS(STATIC_814), i93)
814_0_main_JMP(EOS(STATIC_814), i93) → 848_0_main_Load(EOS(STATIC_848), i93)
848_0_main_Load(EOS(STATIC_848), i93) → 673_0_main_Load(EOS(STATIC_673), i93)
673_0_main_Load(EOS(STATIC_673), i88) → 677_0_main_Inc(EOS(STATIC_677), i88, i88)
745_0_<init>_FieldAccess(EOS(STATIC_745), i93) → 756_0_<init>_Load(EOS(STATIC_756), i93)
756_0_<init>_Load(EOS(STATIC_756), i93) → 762_0_<init>_Load(EOS(STATIC_762), i93)
762_0_<init>_Load(EOS(STATIC_762), i93) → 776_0_<init>_FieldAccess(EOS(STATIC_776), i93)
776_0_<init>_FieldAccess(EOS(STATIC_776), i93) → 799_0_<init>_Return(EOS(STATIC_799), i93)
799_0_<init>_Return(EOS(STATIC_799), i93) → 808_0_main_Store(EOS(STATIC_808), i93)
808_0_main_Store(EOS(STATIC_808), i93) → 817_0_main_JMP(EOS(STATIC_817), i93)
817_0_main_JMP(EOS(STATIC_817), i93) → 861_0_main_Load(EOS(STATIC_861), i93)
861_0_main_Load(EOS(STATIC_861), i93) → 673_0_main_Load(EOS(STATIC_673), i93)
R rules:

Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.

P rules:
677_0_main_Inc(EOS(STATIC_677), x0, x0) → 677_0_main_Inc(EOS(STATIC_677), +(x0, -1), +(x0, -1)) | >(x0, 0)
R rules:

Filtered ground terms:

677_0_main_Inc(x1, x2, x3) → 677_0_main_Inc(x2, x3)
EOS(x1) → EOS
Cond_677_0_main_Inc(x1, x2, x3, x4) → Cond_677_0_main_Inc(x1, x3, x4)

Filtered duplicate args:

677_0_main_Inc(x1, x2) → 677_0_main_Inc(x2)
Cond_677_0_main_Inc(x1, x2, x3) → Cond_677_0_main_Inc(x1, x3)

Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.

P rules:
677_0_main_Inc(x0) → 677_0_main_Inc(+(x0, -1)) | >(x0, 0)
R rules:

Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.

P rules:
677_0_MAIN_INC(x0) → COND_677_0_MAIN_INC(>(x0, 0), x0)
COND_677_0_MAIN_INC(TRUE, x0) → 677_0_MAIN_INC(+(x0, -1))
R rules:

(14) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 677_0_MAIN_INC(x0[0]) → COND_677_0_MAIN_INC(x0[0] > 0, x0[0])
(1): COND_677_0_MAIN_INC(TRUE, x0[1]) → 677_0_MAIN_INC(x0[1] + -1)

(0) -> (1), if (x0[0] > 0 ∧x0[0] →^* x0[1])

(1) -> (0), if (x0[1] + -1 →^* x0[0])

The set Q is empty.

(15) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpCand1ShapeHeuristic@28f2146a Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 0 Max Right Steps: 0

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair 677_0_MAIN_INC(x0) → COND_677_0_MAIN_INC(>(x0, 0), x0) the following chains were created:

We consider the chain 677_0_MAIN_INC(x0[0]) → COND_677_0_MAIN_INC(>(x0[0], 0), x0[0]), COND_677_0_MAIN_INC(TRUE, x0[1]) → 677_0_MAIN_INC(+(x0[1], -1)) which results in the following constraint:
(1)    (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 677_0_MAIN_INC(x0[0])≥NonInfC∧677_0_MAIN_INC(x0[0])≥COND_677_0_MAIN_INC(>(x0[0], 0), x0[0])∧(U^Increasing(COND_677_0_MAIN_INC(>(x0[0], 0), x0[0])), ≥))

We simplified constraint (1) using rule (IV) which results in the following new constraint:
(2)    (>(x0[0], 0)=TRUE ⇒ 677_0_MAIN_INC(x0[0])≥NonInfC∧677_0_MAIN_INC(x0[0])≥COND_677_0_MAIN_INC(>(x0[0], 0), x0[0])∧(U^Increasing(COND_677_0_MAIN_INC(>(x0[0], 0), x0[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_677_0_MAIN_INC(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_677_0_MAIN_INC(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_677_0_MAIN_INC(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)

We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(6)    (x0[0] ≥ 0 ⇒ (U^Increasing(COND_677_0_MAIN_INC(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)

For Pair COND_677_0_MAIN_INC(TRUE, x0) → 677_0_MAIN_INC(+(x0, -1)) the following chains were created:

We consider the chain COND_677_0_MAIN_INC(TRUE, x0[1]) → 677_0_MAIN_INC(+(x0[1], -1)) which results in the following constraint:
(7)    (COND_677_0_MAIN_INC(TRUE, x0[1])≥NonInfC∧COND_677_0_MAIN_INC(TRUE, x0[1])≥677_0_MAIN_INC(+(x0[1], -1))∧(U^Increasing(677_0_MAIN_INC(+(x0[1], -1))), ≥))

We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(8)    ((U^Increasing(677_0_MAIN_INC(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)

We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(9)    ((U^Increasing(677_0_MAIN_INC(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)

We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(10)    ((U^Increasing(677_0_MAIN_INC(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)

We simplified constraint (10) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(11)    ((U^Increasing(677_0_MAIN_INC(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

677_0_MAIN_INC(x0) → COND_677_0_MAIN_INC(>(x0, 0), x0)
- (x0[0] ≥ 0 ⇒ (U^Increasing(COND_677_0_MAIN_INC(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
COND_677_0_MAIN_INC(TRUE, x0) → 677_0_MAIN_INC(+(x0, -1))
- ((U^Increasing(677_0_MAIN_INC(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0
POL(FALSE) = 0
POL(677_0_MAIN_INC(x₁)) = [2]x₁
POL(COND_677_0_MAIN_INC(x₁, x₂)) = [2]x₂
POL(>(x₁, x₂)) = [-1]
POL(0) = 0
POL(+(x₁, x₂)) = x₁ + x₂
POL(-1) = [-1]

The following pairs are in P_>:

COND_677_0_MAIN_INC(TRUE, x0[1]) → 677_0_MAIN_INC(+(x0[1], -1))

The following pairs are in P_bound:

677_0_MAIN_INC(x0[0]) → COND_677_0_MAIN_INC(>(x0[0], 0), x0[0])

The following pairs are in P_≥:

677_0_MAIN_INC(x0[0]) → COND_677_0_MAIN_INC(>(x0[0], 0), x0[0])

There are no usable rules.

(16) Complex Obligation (AND)

(17) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 677_0_MAIN_INC(x0[0]) → COND_677_0_MAIN_INC(x0[0] > 0, x0[0])

The set Q is empty.

(18) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(19) TRUE

(20) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_677_0_MAIN_INC(TRUE, x0[1]) → 677_0_MAIN_INC(x0[1] + -1)

The set Q is empty.

(21) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(0) Obligation:

(1) JBCToGraph (SOUND transformation)

(2) Obligation:

(3) TerminationGraphToSCCProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) SCCToIDPv1Proof (SOUND transformation)

(7) Obligation:

(8) IDPtoQDPProof (SOUND transformation)

(9) Obligation:

(10) QDPSizeChangeProof (EQUIVALENT transformation)

(11) YES

(12) Obligation:

(13) SCCToIDPv1Proof (SOUND transformation)

(14) Obligation:

(15) IDPNonInfProof (SOUND transformation)

(16) Complex Obligation (AND)

(17) Obligation:

(18) IDependencyGraphProof (EQUIVALENT transformation)

(19) TRUE

(20) Obligation:

(21) IDependencyGraphProof (EQUIVALENT transformation)

(22) TRUE